Laurie, Laurie von viewing lasting home

Ja, Herzlich Willkommen Ansage Siehe da

Ja gut, unser heutiges erstes Teilkapitel, das wird uns jetzt nicht die ganze Sitzung

beschäftigen, aber vielleicht so die erste Hälfte, lautet kurz Induktion mehrsortig,

also genauer gesagt Induktion über mehrsortigen Datentypen,

noch genauer gesagt Induktion und Rekursion über mehrsortigen Datentypen,

denn das haben wir uns ja noch nicht auf den Detail angesehen.

Ich erinnere nochmal an unser Hauptbeispiel eines mehrsortigen Datentyps, das ist dieser hier.

Dieser hier.

Unser Datentyp von beliebig geordnet verzweigenden Bäumen.

Mit vier Konstruktoren, zwei für Bäume, zwei für Wälder.

Nicht einmal dieser Leaf-Konstruktor, der uns also einen Baum, der nur aus einem Blatt besteht, bastelt.

Und die Blätter sind beschriftet mit Elementen unseres Parametertyps ab.

Dann der Node-Konstruktor, der aus einem Wald, also effektiv einer Liste von Bäumen,

einen Knoten konstruiert, der gerade diese gegebenen Bäume als Kinder hat.

Dann ein Konstruktor nil, der konstruiert uns einen leeren Wald.

Und ein Konstruktor cons, der sich verhält wie ein Listenkonstruktor, nur eben für Listen von Bäumen.

Also einen Baum und einen Forest und baut uns einen neuen Forest, in dem dieser Baum gerade vorne dran gehängt wird.

So, das ist das eine, was wir jetzt als Erinnerung brauchen.

Wir werden jetzt zunächst mal nochmal uns ansehen,

wie man Funktionen auf solchen mehrsortigen Datentypen definiert.

Wir haben das im Prinzip jetzt gesehen,

also mehrsortige Datentypen sind also initial als mehrsortige Algebren.

Und Initialität heißt, wenn ich irgendeine weitere mehrsortige Algebra des selben Typs angebe,

dann bekomme ich einen eindeutigen Homomorphismus, was eben hinausläuft auf eine Familie von Abbildungen oder Funktionen,

die eine Homomorphiebedingung erfüllen, mit anderen Worten eine rekursive Gleichung.

Man verschafft sich daraus dann auf dieselbe Weise wie im Einsortigen ein primitives Rekursionsprinzip,

wo ich also auf der rechten Seite von Rekursiven Definitionen erstens Rekursive Aufrufe verwenden darf,

also Rekursive Aufrufe auf die Argumente von Konstruktorpattern, die ich auf der linken Seite hinschreibe,

und wo ich außerdem noch die Argumente weiter verwenden darf.

Das exerzieren wir jetzt nicht auf den Detail noch durch.

Die Hauptmessage ist, diese Funktionen sind Familien von Funktionen.

Also ein Homomorphismus von mehrsortigen Algebren ist eine mehrsortige Funktion.

Das heißt, wenn wir jetzt rekursiv definieren Funktionen auf solchen mehrsortigen Datentypen,

dann definieren wir auch mehrsortige Funktionen.

Das heißt, wir definieren mehrere Funktionen auf einmal durch gegenseitige Rekursionen.

Und zwar eine Funktion pro echt neu eingeführten Datentyp.

Wir haben gesehen, das Ding hier ist grundsätzlich dreisortig, aber eine der drei Sorten ist also die Parameter-Sorte A.

Und die Definition von Sigma-Homomorphismen in dem Falle hat ja gesagt,

gut, auf den Parameter-Sorten definiere ich effektiv nichts, sondern nur Identität.

Das heißt, wir definieren immer, wenn wir hier was rikursiv definieren, zwei Funktionen,

eine auf Bäumen und eine auf Wäldern.

So, und das machen wir jetzt mal.

Wir nennen die Funktionen, die wir definieren, weil sie oft ähnliche Dinge tun,

typischerweise zweimal ungefähr gleich und unterscheiden sie nur durch so einen angehängten letzten Buchstaben,

der also andeutet, ob sie jetzt gerade auf Bäumen oder auf Wäldern arbeitet.

Also mirrorty zum Beispiel ist also ein Teil von, also eine Hälfte von so einem Funktionenpaar,

was jetzt also auf Bäumen arbeitet.

Was ich machen will, ist, ich will so einen Baum, wie der Name der Funktion schon sagt, spiegeln.

So, das heißt, das ist jetzt eine Funktion von 3a nach 3a und der steht gegenüber